T:Type, l1, l2:(T List). fseg(T;l1;l2)  (||l1||  ||l2||) 

latex

ProofTree

Definitions	s = t, t  T, x:AB(x), x:A. B(x), ||as||, Type, type List, as @ bs, , n+m, A  B, i  j , , True, P  Q, P  Q, T, x:A  B(x), P & Q, P  Q, x:A. B(x), fseg(T;L1;L2)
Lemmas	iff wf, rev implies wf, le wf, squash wf, true wf, length append, non neg length, length wf1